\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $T$:Type, ${\it ks}$:Knd List, ${\it upd}$:update{-}spec(${\it ds}$;${\it da}$),\+
\\[0ex]$a$:($\mathbb{N}\rightarrow$($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$) \}$\rightarrow$State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$$T$$\rightarrow\mathbb{B}$)).
\-\\[0ex]$\neg$"ecl" $\in$ dom(${\it ds}$)
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ Normal(${\it da}$)
\\[0ex]$\Rightarrow$ ($\forall$$k$$\in$${\it ks}$. isrcv($k$) $\Rightarrow$ $i$ $=$ destination(lnk($k$)) $\in$ Id)
\\[0ex]$\Rightarrow$ update{-}spec{-}decl(${\it upd}$;${\it ds}$)
\\[0ex]$\Rightarrow$ \=ecl{-}machine2($i$;${\it ds}$;${\it da}$;"ecl";$T$;${\it ks}$;$a$;${\it upd}$)\+
\\[0ex]$\Vdash$ ${\it es}$.\=$\forall$$z$$\in$update{-}spec{-}vars(${\it upd}$).\+
\\[0ex]es{-}decls(${\it es}$;$i$;${\it ds}$ $\oplus$ "ecl" : $T$;${\it da}$)
\\[0ex]$\Rightarrow$ \=vartype($i$;$z$) $\subseteq\rho$ ${\it ds}$($z$)\+
\\[0ex]\& \=$\forall$$e$@$i$.\+
\\[0ex]$\forall$${\it e'}$$\geq$$e$.\=($z$ after ${\it e'}$)\+
\\[0ex]$=$
\\[0ex]es{-}trans{-}state{-}from\{i:l\}(\=${\it es}$;${\it ks}$;\+
\\[0ex]$\lambda$$k$,$s$,$v$,${\it z'}$.
\\[0ex]list\_accum(\=${\it z'}$,${\it nf}$.\=${\it nf}$/$n$,$f$.\+\+
\\[0ex]if \=$a$($n$,$k$,$s$,$v$,$s$("ecl"))$\rightarrow$\+
\\[0ex]$f$($s$,$v$)
\-\\[0ex]else ${\it z'}$ fi;
\-\\[0ex]${\it z'}$;
\\[0ex]${\it upd}$($\langle$$k$$,\,$$z$$\rangle$)?nil);$z$ when $e$;$e$;${\it e'}$)
\-\-\\[0ex]$\in$ ${\it ds}$($z$)
\-\-\-\-\-
\end{tabbing}